package com.googlecode.kipler.satisfiability.completion.branching;

import java.util.HashSet;
import java.util.Set;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.DependencySet;
import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.container.dl.SHOIQIndividual;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.container.dl.operational.IndividualNameManager;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.concept.InequalityConstructor;
import com.googlecode.kipler.syntax.concept.Nominal;
import com.googlecode.kipler.syntax.concept.QualifiedNoRestriction;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.Formula;
import com.googlecode.kipler.syntax.formula.ObjectRoleAssertion;
import com.googlecode.kipler.syntax.formula.SameIndividualAssertion;

/**
 * 
 * @author İnanç Seylan
 * 
 */
public class NominalGuessBranchingPoint extends BranchingPoint {
	private int m = 1;

	private Individual individual;

	private ABox aBox;

	private WorldConstraintSystem newWcs;

	private boolean lastTry;

	private DependencySet dependencySet = new DependencySet();

	private Formula branchCause;

	public Formula getBranchCause() {
		return branchCause;
	}

	public void setBranchCause(Formula branchCause) {
		this.branchCause = branchCause;
	}

	public Individual getIndividual() {
		return individual;
	}

	public void setIndividual(Individual individual) {
		this.individual = individual;
	}

	private QualifiedNoRestriction getOriginalQR() {
		ConceptAssertion ca = (ConceptAssertion) getBranchCause();
		return (QualifiedNoRestriction) ca.getConcept();
	}

	@Override
	public boolean isBranchingPossible() {
		return m <= getOriginalQR().getNo();
	}

	@Override
	public WorldConstraintSystem nextBranch() throws UnsatisfiableException {
		/*
		 * last branching's dependency set is empty in the first iteration, and
		 * it is set with clash dependencies of the previous branching in the
		 * other iterations.
		 */
		dependencySet.addAll(getLastBranchDependencies());
		QualifiedNoRestriction originalQr = getOriginalQR();
		if (m < originalQr.getNo()) {
			newWcs = getWcs().copy();
			newWcs.setId(getWcs().getId() + 1);
		} else if (m == originalQr.getNo()) { // last try
			dependencySet.remove(getWcs());
			newWcs = getWcs();
			lastTry = true;
		}
		QualifiedNoRestriction qr = new QualifiedNoRestriction(
				InequalityConstructor.AT_MOST, m++, originalQr.getRole(), originalQr
						.getConcept());
		aBox = newWcs.getWorld(getWorld().getName()).getABox();
		ConceptAssertion newAtMost = new ConceptAssertion(qr, getIndividual()
				.getName());
		manageDependency(newAtMost);
		newWcs.getData().getLogger().info(
				"WCS " + newWcs.getId() + " Nominal guess rule: Adding "
						+ newAtMost);
		aBox.add(newAtMost);
		Set<Individual> newFillers = new HashSet<Individual>();
		for (int i = 0; i < qr.getNo(); i++) {
			String newIndvName = IndividualNameManager.getInstance()
					.generateIndividualName();
			ObjectRoleAssertion or = new ObjectRoleAssertion(qr.getRole(),
					getIndividual().getName(), newIndvName);
			manageDependency(or);
			ConceptAssertion ca1 = new ConceptAssertion(qr.getConcept(),
					newIndvName);
			manageDependency(ca1);
			ConceptAssertion ca2 = new ConceptAssertion(
					new Nominal(newIndvName), newIndvName);
			manageDependency(ca2);
			newWcs.getData().getLogger().info(
					"WCS " + newWcs.getId() + " Nominal guess rule: Adding "
							+ or + ", " + ca1 + ", and " + ca2);
			aBox.add(or);
			aBox.add(ca1);
			aBox.add(ca2);
			SHOIQIndividual successor = (SHOIQIndividual) aBox
					.getIndividual(newIndvName);
			arrangeLevel(successor);
			assertDifferent(successor, newFillers);
			newFillers.add(successor);
		}
		return newWcs;
	}

	private void arrangeLevel(SHOIQIndividual successor) {
		int level = ((SHOIQIndividual) getIndividual()).getLevel();
		successor.setLevel(level + 1);
	}

	private void assertDifferent(Individual indv1, Set<Individual> individuals)
			throws UnsatisfiableException {
		for (Individual indv2 : individuals) {
			SameIndividualAssertion ia = new SameIndividualAssertion(indv1
					.getName(), indv2.getName()).toggleNegated();
			if (indv1 != indv2 && !aBox.contains(ia)) {
				manageDependency(ia);
				newWcs.getData().getLogger().info(
						"WCS " + newWcs.getId()
								+ " Nominal guess rule: Adding " + ia);
				aBox.add(ia);
			}
		}
	}

	private void manageDependency(Formula f) {
		if (lastTry) {
			newWcs.getData().getDependencyManager().move(f, getBranchCause());
			newWcs.getData().getDependencyManager().addAll(f, dependencySet);
		} else {
			newWcs.getData().getDependencyManager().add(f, getWcs());
		}
	}

	@Override
	public void backtrack() {
		// TODO Auto-generated method stub

	}

}
